Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:
Proving the Blakers-Massey theorem in any -topos and with the (n-connected, n-truncated) factorization system allowed to be replaced by more general modalities:
On combining homotopy type theory with opetopic type theory (for higher algebra):
reviewed in:
Eric Finster, Towards Higher Universal Algebra in Type Theory, Homotopy Type Theory Electronic Seminar 2018 (recording, Agda code)
Eric Finster, The -category of Types, talk at CQTS (Dec 2022) [slides: pdf, video: rec]
Abstract: A major outstanding difficulty in Homotopy Type Theory is the description of coherent higher algebraic structures. As an example, we know that the algebraic structure possessed by the collection of types and functions between them is not a traditional 1-category, but rather an (∞,1)-category. In this talk, I will describe how the addition of a finite collection of additional definitional equalities designed to render the notion of “opetopic type” definable in fact allows one to construct the (∞,1)-category structure on the universe of types.
On homotopy dependent linear type theory of dependent stable homotopy types with categorical semantics in parametrized spectra:
On weak -categories via computads construed as inductive types:
On the tangent (infinity,1)-topos of parameterized spectra:
Last revised on July 13, 2024 at 07:55:52. See the history of this page for a list of all contributions to it.